Nuprl Lemma : atomic_wf
2,24
postcript
pdf
a
:
. atomic(
a
)
Prop
latex
Definitions
atomic(
a
)
,
P
&
Q
,
Prop
,
a
~
b
,
A
,
reducible(
a
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
reducible
wf
,
not
wf
,
assoced
wf
origin
a:
. atomic(a) 
Prop a:. atomic(a) Prop 
Ax:A. B(x) T